(set-logic QF_BV)
(declare-fun _substvar_1152_ () Bool)
(declare-fun _substvar_1066_ () Bool)
(declare-fun _substvar_324_ () (_ BitVec 8))
(declare-fun _substvar_1065_ () Bool)
(declare-fun _substvar_354_ () (_ BitVec 16))
(declare-fun _substvar_393_ () (_ BitVec 16))
(declare-fun _substvar_1028_ () Bool)
(declare-fun _substvar_402_ () (_ BitVec 16))
(declare-fun _substvar_395_ () (_ BitVec 16))
(declare-fun _substvar_322_ () (_ BitVec 8))
(declare-fun _substvar_394_ () (_ BitVec 16))
(declare-fun _substvar_1190_ () Bool)
(declare-fun _substvar_386_ () (_ BitVec 16))
(declare-fun _substvar_1021_ () Bool)
(assert (and true true true true true true true true true true true true (= _substvar_394_ (bvor (bvshl _substvar_386_ (_ bv8 16)) ((_ zero_extend 8) _substvar_324_))) (= _substvar_395_ (bvor (_ bv0 16) ((_ zero_extend 8) _substvar_322_))) true true true true true _substvar_1065_ true true true (bvult _substvar_394_ _substvar_395_) true true _substvar_1152_ (bvult _substvar_393_ _substvar_394_) true true true true true true true true true true _substvar_1190_ (bvult _substvar_402_ _substvar_393_) true true true true true true true true true true true true true true true true true true true true true true true (bvult _substvar_354_ _substvar_402_) true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true true _substvar_1021_ true true true true true true true _substvar_1028_ true true true true true true true true true true true _substvar_1066_))
(check-sat)
(exit)
